Skip to content

Add BitPack instance for Index 0 #2784

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
kleinreact wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add BitPack instance for Index 0 #2784

kleinreact wants to merge 3 commits into from

Conversation

@kleinreact
Copy link
Member

@kleinreact kleinreact commented Aug 7, 2024 •
edited
Loading

This PR gets rid of the additional 1 <= n constraint for the BitPack instance of Index n.

Background:

  • Index 0 and Void are empty types → isomorphic to the empty set
  • Index 1 and () are singleton types → isomorphic to a singleton set

Hence, we only need to question ourselves: how many bits do you need to distinguish between different elements of these types / sets? In both cases the answer clearly is: 0. Thus, BitSize (Index 0) = 0.

From another perspective: Clash generates valid HDL for Index 0 and the number of bits required by the generated HDL is zero as well. Hence, there is no reason to hide this fact in the type system for this particular case.

Requires:

Still TODO:

  • Add this fact to the typelits plugins.
  • Write a changelog entry (see changelog/README.md)
  • Check copyright notices are up to date in edited files

martijnbastiaan
martijnbastiaan requested changes Aug 8, 2024
View reviewed changes
Copy link
Member

@martijnbastiaan martijnbastiaan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review together with @DigitalBrains1

Nice, this would get rid of a lot of unwanted 1 <= n constraints.

Add this fact to the typelits plugins.

I doubt reasoning about type families is in-scope for the plugins, but you might want to take that up with the maintainers :-).

I think we should change the cover letter's motivation to be something along the lines of "this aligns clash-the-compiler's thoughts on Index 0 with BitPack (Index 0)".

A changelog is needed, but that's also in the TODOs.

Other than that LGTUs.

@DigitalBrains1
Copy link
Member

DigitalBrains1 commented Aug 8, 2024 •
edited
Loading

It seems to still need something more though:

src/Clash/Explicit/Synchronizer.hs:126:35: error: [GHC-25897]
    • Could not deduce ‘Clash.Sized.Internal.Index.BitSizeIndex
                          (2 ^ addrSize)
                        ~ addrSize’
      from the context: (KnownDomain wdom, KnownDomain rdom, NFDataX a,
                         KnownNat addrSize, 1 <= addrSize)
Full message 
src/Clash/Explicit/Synchronizer.hs:126:35: error: [GHC-25897]
    • Could not deduce ‘Clash.Sized.Internal.Index.BitSizeIndex
                          (2 ^ addrSize)
                        ~ addrSize’
      from the context: (KnownDomain wdom, KnownDomain rdom, NFDataX a,
                         KnownNat addrSize, 1 <= addrSize)
        bound by the type signature for:
                   fifoMem :: forall (wdom :: Clash.Signal.Internal.Domain)
                                     (rdom :: Clash.Signal.Internal.Domain) a
                                     (addrSize :: GHC.TypeNats.Nat).
                              (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
                               1 <= addrSize) =>
                              Clock wdom
                              -> Clock rdom
                              -> Enable wdom
                              -> Enable rdom
                              -> Signal wdom Bool
                              -> Signal rdom (BitVector addrSize)
                              -> Signal wdom (BitVector addrSize)
                              -> Signal wdom (Maybe a)
                              -> Signal rdom a
        at src/Clash/Explicit/Synchronizer.hs:(100,1)-(115,18)
      Expected: BitVector addrSize
                -> Clash.Sized.Internal.Index.Index (2 ^ addrSize)
        Actual: BitVector
                  (Clash.Class.BitPack.Internal.BitSize
                     (Clash.Sized.Internal.Index.Index (2 ^ addrSize)))
                -> Clash.Sized.Internal.Index.Index (2 ^ addrSize)
      ‘addrSize’ is a rigid type variable bound by
        the type signature for:
          fifoMem :: forall (wdom :: Clash.Signal.Internal.Domain)
                            (rdom :: Clash.Signal.Internal.Domain) a
                            (addrSize :: GHC.TypeNats.Nat).
                     (KnownDomain wdom, KnownDomain rdom, NFDataX a, KnownNat addrSize,
                      1 <= addrSize) =>
                     Clock wdom
                     -> Clock rdom
                     -> Enable wdom
                     -> Enable rdom
                     -> Signal wdom Bool
                     -> Signal rdom (BitVector addrSize)
                     -> Signal wdom (BitVector addrSize)
                     -> Signal wdom (Maybe a)
                     -> Signal rdom a
        at src/Clash/Explicit/Synchronizer.hs:(100,1)-(115,18)
    • In the first argument of ‘fmap’, namely ‘unpack’
      In the second argument of ‘(<$>)’, namely ‘fmap unpack waddr’
      In the first argument of ‘(<*>)’, namely
        ‘RamWrite <$> fmap unpack waddr’
    • Relevant bindings include
        portB :: Signal wdom (RamOp (2 ^ addrSize) a)
          (bound at src/Clash/Explicit/Synchronizer.hs:125:4)
        waddr :: Signal wdom (BitVector addrSize)
          (bound at src/Clash/Explicit/Synchronizer.hs:116:38)
        raddr :: Signal rdom (BitVector addrSize)
          (bound at src/Clash/Explicit/Synchronizer.hs:116:32)
        fifoMem :: Clock wdom
                   -> Clock rdom
                   -> Enable wdom
                   -> Enable rdom
                   -> Signal wdom Bool
                   -> Signal rdom (BitVector addrSize)
                   -> Signal wdom (BitVector addrSize)
                   -> Signal wdom (Maybe a)
                   -> Signal rdom a
          (bound at src/Clash/Explicit/Synchronizer.hs:116:1)
    |
126 |                (RamWrite <$> fmap unpack waddr <*> fmap fromJustX wdataM)
    |                                   ^^^^^^

Experienced with GHC 9.6.6.

[edit]
This also happens on CI with multiple (perhaps all? Didn't check) GHC versions.
[/edit]

@kleinreact
Copy link
Member Author

kleinreact commented Aug 8, 2024

It's because of the new BitSizeIndex type family introduced and can be fixed by teaching the typelits plugins about it's properties in particular. Unfortunately, I also don't know about any better solution at the moment. I tried several other things to help the type checker in acting in any smarter way, but that's the best solution I could find.

@kleinreact kleinreact force-pushed the add-bitpack-for-index-zero branch from 8510fbd to 2714056 Compare September 1, 2024 19:34
@kleinreact kleinreact mentioned this pull request Sep 2, 2024
Merged
2 tasks
@leonschoorl
Copy link
Member

leonschoorl commented Oct 3, 2024

I understand the desire to get rid of that 1 <= n constraint in a polymorphic setting.

But lets say someone is (accidentally) calling unpack @(Index 0).
This PR changes this from a compile time error to a run time error.
Which feels to me like a step in the wrong direction.

@kleinreact
Copy link
Member Author

kleinreact commented Oct 4, 2024

This PR changes this from a compile time error to a run time error.

I don't think that this is the right way to look at it. Consider the following example:

topEntity ::
  HiddenClockResetEnable System =>
  Signal System (Index 0)
topEntity = pure $ unpack @(Index 0) $ resize (0 :: BitVector 1)

If that description is turned into Verilog with clash, without the changes of this PR, then the example produces a compile time error. However, it produces perfectly valid Verilog after the fixes introduced by this PR.

I agree that the user might end up with a run time error in simulation, if trying to inspect what comes out of applying unpack @(Index 0), but that is fine, as there is no output unpack @(Index 0) can ever produce. Thus, the error is not that unpack @(Index 0) now is a valid object, which can be created at runtime, but more that the user tries to get something out of it, which just is not possible.

Note that the type system never was intended to prevent us from this, in the same way as it cannot prevent us from ever having a look at the contents of undefined.

@kleinreact kleinreact force-pushed the add-bitpack-for-index-zero branch from 2714056 to 0103c88 Compare October 4, 2024 15:50
@kleinreact kleinreact force-pushed the add-bitpack-for-index-zero branch from 0103c88 to 8f922b8 Compare November 23, 2025 19:59
@kleinreact kleinreact marked this pull request as ready for review November 23, 2025 20:04
DigitalBrains1
DigitalBrains1 requested changes Nov 24, 2025
View reviewed changes
Copy link
Member

@DigitalBrains1 DigitalBrains1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This isn't a full review yet; I'll wait until you have it working.

But browsing a bit I did notice you expanded the scope of the PR a lot. You've removed a lot of Index n, 1 <= n constraints even if they don't involve BitPack. If you want to address different cases of Index bounds as well, I think it's better treated in a new PR because it'll require some good thought.

For instance, you're removing the 1 <= n from the resetGlitchFilter functions, but now it is just completely broken:

>>> printX $ sampleN 10 $ unsafeFromReset $ resetGlitchFilter d2 systemClockGen resetGen
[True,True,True,True,True,False,False,False,False,False]
>>> printX $ sampleN 10 $ unsafeFromReset $ resetGlitchFilter d0 systemClockGen resetGen
[True,True,True,True,undefined,undefined,undefined,undefined,undefined,undefined]

@kleinreact
Copy link
Member Author

kleinreact commented Nov 24, 2025

But browsing a bit I did notice you expanded the scope of the PR a lot. You've removed a lot of Index n, 1 <= n constraints even if they don't involve BitPack. If you want to address different cases of Index bounds as well, I think it's better treated in a new PR because it'll require some good thought.

Thanks for the quick feedback. I primarily was interested in observing which code may change and just wanted to get some feedback from CI. Unfortunately, there won't be any reasonable feedback without also hiding the warnings currently blocking #3061.

I'll definitely have a closer look on all the introduced changes again.

@kleinreact kleinreact mentioned this pull request Dec 3, 2025
Open
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@martijnbastiaan martijnbastiaan martijnbastiaan requested changes

@rowanG077 rowanG077 rowanG077 left review comments

@DigitalBrains1 DigitalBrains1 DigitalBrains1 requested changes

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@kleinreact @DigitalBrains1 @leonschoorl @martijnbastiaan @rowanG077